package systemfnomabss.syntax


import sybrevolutions.forvalues._
trait Binding {//  self: Binding => 
  type Name
  
  trait Primitive
  type Binds[x] //each instance of binds should have an instance of Nominal

  trait Nominal[Self] {
    //def self:Self
    def swap(a: Name, b: Name): Self
    def fresh(a: Name): Boolean
    def supp: List[Name]
  }
  
  trait PrimitiveNominal[UpTo, Self <: UpTo with Primitive] extends Nominal[UpTo] {this:Self =>
    def fresh(a:Name) = true
    def supp: List[Name]=Nil
    def swap(a:Name, b:Name) = this
  }
  
  
  /*
  
  trait NominalByProxyUpBound[TermType,Self <:TermType] extends Nominal[TermType] {
    //input
    def nomproxy: Nominal[Self]
    
    
    def swap(a:Name,b:Name):TermType = nomproxy.swap(a,b)
    def fresh(a:Name) = nomproxy.fresh(a)
    def supp = nomproxy.supp
    
    //should be ok in subclass
    //assume (nomproxy != null, "creating NomByProxyUpBound but nomproxy null")
  }
  */
    
  /*
  
  implicit def Char2Primitive(s:Char)= new Primitive {}
  implicit def Int2Primitive(s:Int)= new Primitive {}
  implicit def Unit2Primitive(s:Unit)=new Primitive {}
  
  def PrimitiveIsNominal[P <% Primitive](p: P) = new Nominal[P]{
    def self:P = p
    def fresh(a: Name)=true
    def supp: List[Name]=Nil
    def swap(a: Name, b: Name) = self
  }
  def PrimitiveIsNominalByProxy[TermType, P<:TermType](p:P)(implicit prim:P=>Primitive) :Nominal[TermType]=new Nominal[TermType] {
    def self:P = p
    def fresh(a:Name) = true
    def supp: List[Name]=Nil
    def swap(a:Name, b:Name) = self
  }
  
  implicit def IntIsNominal(s: Int) : Nominal[Int] = PrimitiveIsNominal(s)
  implicit def CharIsNominal(s: Char): Nominal[Char] = PrimitiveIsNominal(s)
  implicit def UnitIsNominal(s: Unit): Nominal[Unit] = PrimitiveIsNominal(s)
  
// can't abstract over Iterable here because it isn't defined like that in std lib
  
  implicit def ListIsNominal[T <% Nominal[T]](self: List[T]): Nominal[List[T]] = new Nominal[List[T]] {
    def swap(a: Name, b: Name) = self map (_.swap(a, b))    
    def fresh(a: Name) = self forall (_.fresh(a))
    def supp = (self flatMap (_.supp)).toList
  }   
  
  implicit def OptionIsNominal[T <% Nominal[T]](self: Option[T]): Nominal[Option[T]] = new Nominal[Option[T]] {
    def swap(a: Name, b: Name) = self map (_.swap(a, b))    
    def fresh(a: Name) = self forall (_.fresh(a))
    def supp = (self.toList flatMap (_.supp)).toList
  }     
  
  implicit def SetIsNominal[T <% Nominal[T]](self: Set[T]): Nominal[Set[T]] = new Nominal[Set[T]] {
    def swap(a: Name, b: Name) = self map (_.swap(a, b))    
    def fresh(a: Name) = self forall (_.fresh(a))
    def supp = (self flatMap (_.supp)).toList
  }     
  */
  
}



trait BindingSyntax extends Binding{ //self: Binding  with BindingSyntax => //self: AbsM with Binding with Substitution with BindingSyntax =>
//trait Equality[T] {
//      def ===(a: T): Boolean
//}

type Tag = Int

type Node
//def NodeIsNominalStub(n:Node):Nominal[Node]

object Name {
  private[Name] var nextTag: Int = -1 // only for toString
  def apply(name:Name) = new Name(name.name)
  def apply(name:String) = new Name(name)
}
class Name(val name: String) extends Nominal[Name] {
  def \\[T](body: T)(implicit c: T => Nominal[T]): \\[T] = new \\[T](this, body)
  
  override def equals(o: Any): Boolean =  o match {
    case n: Name  => n eq this //if n.tag == t => true
    case _ => false
  }
  
  def swap(a: Name, b: Name) = if(this == a) b else if(this == b) a else this
  def fresh(a: Name) = this != a
  def supp = List(this)    
  val tag:Tag =  {Name.nextTag +=1; Name.nextTag}
  override def toString = name + "$" + tag
}
implicit  val NameTypeMan : TypeMan[Name] = new sybrevolutions.forvalues.PrimitiveTypeMan("name")

//def gensym(s: String): AM[Name] = for( t <- AM.newTag) yield Name(t, s)
//def rename(a: Name): AM[Name] = for( t <- AM.newTag) yield Name(t, a.s) //subsumed by name.apply




type Binds[x] = \\[x] //just set equal to \\ if you use just one
def BindsIsNominal[T](b:Binds[T]):Nominal[Binds[T]] = b

object \\ {
  def apply[T](binder: Name, body: T)(implicit c: T => Nominal[T]) = new \\[T](binder, body)
  def unapply[T](scrutinee: \\[T])(implicit c: T => Nominal[T]): Option[(Name, T)] = Some(scrutinee unabs)
}

class \\[T](private[BindingSyntax] val binder: Name, private[BindingSyntax] val body: T)(
            implicit val bodynom: T => Nominal[T]) extends Nominal[\\[T]] {
      
  def unabs: (Name, T) = { val newBinder = Name(binder);  
                             (newBinder, body swap (binder, newBinder)) }
      
  override def equals(o: Any): Boolean = o match {
    case other: \\[T] => (binder == other.binder && body == other.body) ||  // TODO: unchecked!
        (other.body.fresh(binder) && body == other.body.swap(binder, other.binder))
    case _ => false
  }

  
  //def gequals[Eq[x] <: Equality[x] ](other: \\[T])(implicit neq: Name => Eq[Name], beq: T => Eq[T]): Boolean = (binder === other.binder) && (body === other.body) ||  // TODO: unchecked!
  //      (other.body.fresh(binder) && (body === other.body.swap(binder, other.binder)))
  
  def swap(a: Name, b: Name) = \\(binder swap(a, b), body swap(a, b)) // boilerplate
  def fresh(a: Name) = if(a == binder) true else body fresh (a)
  def supp = body.supp filter (_ != binder)        
  
  override def toString = {// val (binder,body) = unabs;
                            binder + "\\\\" + body }
  }
      //for(
      //bibo <- unabs;             
      //val (binder, body) = bibo)
      //yield binder + "\\\\" + body).run // NOTE: only useful for local debug output*/
 //}
 
   

/*
   * Generic function definitions
   */
     
  //use to layer nominal on spineview
  class GenNominal[Self]( val self:Self)(implicit val tyman:TypeMan[Self]) extends Nominal[Self]{
    assume (tyman != null, "creating gennominal with tyman null: "+self)
    def swap(a: Name, b: Name): Self = (swapnames_gen(tyman.toValSpine(self))(a,b)).buildFromSpine
    def fresh(a: Name):Boolean  = freshname_gen(tyman.toValSpine(self))(a)
    def supp: List[Name] = suppnames_gen(tyman.toValSpine(self))
  }

  trait GenNominalByProxy[TermType, Self<: TermType] extends Nominal[TermType] {this: Self =>
    //input
    //this lazy val should override the def above, which ideally would be an abstract lazy val, but that's not possible
    //collapsed hierarchy to enable lazy val
    lazy val nomproxy:Nominal[Self] = {assume (( typeman != null), "generating nomproxy with typeman null for "+this)
      new GenNominal[Self](this)(typeman) {}
    }
    def swap(a:Name,b:Name):TermType = nomproxy.swap(a,b)
    def fresh(a:Name) = nomproxy.fresh(a)
    def supp = nomproxy.supp

    //how do we get typeman inserted early enough? skip doing it implicitly for now, just let implementing nodes make the link explicitly
    val typeman:TypeMan[Self]
  }
  

  def swapnames[T](a: Name, b: Name)(t:T)(implicit tman: TypeMan[T]):T = t match {
    //case tn: Name => tn.swap(a,b) . asInstanceOf[T]
    //case tb: Binds[y]=> BindsIsNominal(tb).swap(a,b).asInstanceOf[T]
    case trumps: Nominal[T] => trumps.swap(a,b)
    case _ => {new Exception("Applying workfunctiondispatch on illegal type: trying spineview impl").printStackTrace();
      swapnames_gen(tman.toValSpine(t))(a,b).buildFromSpine}
  }
  def swapnames_gen[T](ts:ValSpine[T])(a:Name,b:Name):ValSpine[T] = ts match {
    case ConstrExt(_,_) => ts
    case Apped(deep,Typed(arg,tman))=> {
      Apped(swapnames_gen(deep)(a,b), Typed(swapnames(a,b)(arg)(tman),tman))
    }
  }


  def freshname[T](a:Name)(t:T)(implicit tman: TypeMan[T]):Boolean = t match {
    //case tn: Name => tn.fresh(a)
    //case tb: Binds[y] => BindsIsNominal(tb).fresh(a)
    case trumps: Nominal[T] => trumps.fresh(a)
    case _ => {new Exception("Applying workfunctiondispatch on illegal type: trying spineview impl").printStackTrace();
      freshname_gen(tman.toValSpine(t))(a)}
  }
  def freshname_gen[T](ts:ValSpine[T])(a:Name):Boolean = ts match {
      case ConstrExt(_,_) => true
      case Apped(deep,Typed(arg,tman))=> freshname(a)(arg)(tman) && freshname_gen(deep)(a)
  }
  
  def suppnames[T](t:T)(implicit tman: TypeMan[T]):List[Name] = t match {
    //case tn: Name => println("supp match Name "+t);/*NameIsNominal*/(tn).supp
    //case tb: Binds[y] => println("supp match Binds "+t);BindsIsNominal(tb).supp
    case trumps: Nominal[T] => trumps.supp
    case _ => {new Exception("Applying workfunctiondispatch on illegal type: trying spineview impl").printStackTrace();
      suppnames_gen(tman.toValSpine(t))}
    /*
    if (t.isInstanceOf[Name]) List(t.asInstanceOf[Name]) else 
    if (t.isInstanceOf[Binds[x] forSome{type x}]) BindsIsNominal(t.asInstanceOf[Binds[x] forSome{type x}]).supp else
    suppnames_gen(tman.toValSpine(t))
    */
  }
  def suppnames_gen[T](ts:ValSpine[T]):List[Name] = ts match {
    case ConstrExt(_,_) => List()
    case Apped(deep,Typed(arg,tman)) => suppnames(arg)(tman) ::: suppnames_gen(deep)
  }
  



  
  
  
  /*
    trait GenWorkFunctionDispatcher[T] {
      type resulttype
      val onName : (Nominal[Name])=>resulttype
      def onBinds[y]: (Nominal[Binds[y]])=>resulttype
      def onPrimitive: (Nominal[Primitive])=>resulttype
      def onNode: (Nominal[Node]) => resulttype
      def onGeneric: (ValSpine[T]=>resulttype)
      
      def apply(t:T)(implicit tman: TypeMan[T]):resulttype = t match {
        case tn: Name => onName(/* NameIsNominal*/(tn) )
        case tb: Binds[y] => onBinds(BindsIsNominal(tb))
        case prim: Primitive => onPrimitive( PrimitiveIsNominal(prim))
        //case node: Node  => onNode(NodeIsNominalStub(node))
        case _ => {new Exception("Applying workfunctiondispatch on illegal type: trying spineview impl").printStackTrace();
                  onGeneric(tman.toValSpine(t))}
      }
    }
    */
    /*
    class swapnames2[T](a:Name,b:Name) extends GenFunction[T] {
      type resulttype = T
      def onconc[X] :(Nominal[X])=>T =(nom:Nominal[X])=> nom.swap(a,b).asInstanceOf[T] 
      val onName = onconc[Name]
      def onBinds[y] = onconc[Binds[y]]
      def onPrimitive = onconc[Primitive]
      def onGeneric = (vs: ValSpine[T])=> swapnames_gen(vs)(a,b).buildFromSpine
    }
    */

}

trait Substitution { self: Binding with BindingSyntax with Substitution => // self: AbsM  with Binding with BindingSyntax with Substitution =>
type Name

trait Substable[SubstParam, Self] { 
  //def apply(se:Self):Substable[SubstParam,Self]
  def subst(sub: Name => Option[SubstParam]): Self
  def subst(n: Name, r: SubstParam): Self = subst{case y if n == y => Some(r) case _ => None }
}

class SubstTo[S] {
  type Subst[T] = Substable[S, T]

  implicit def OptionIsSubstable[T <% Subst[T]](self: Option[T]): Subst[Option[T]] = new Substable[S, Option[T]] {
    def subst(sub: Name => Option[S]): Option[T] = self.map(_.subst(sub))
  }

  implicit def SetIsSubstable[T <% Subst[T]](self: Set[T]): Subst[Set[T]] = new Substable[S, Set[T]] {
   def subst(sub: Name => Option[S]): Set[T] = self.map(_.subst(sub))
  }
}

class AbsSubstTo[S] {
  type Subst[T] = Substable[S, T]
  
  implicit def AbsIsSubstable[T](self: \\[T])(implicit c: T => Subst[T]): Subst[\\[T]] = new Substable[S, \\[T]]  {
    implicit val cn: T => Nominal[T] = self.bodynom
    def subst(sub: Name => Option[S]): \\[T] =  self match {
      case \\(binder, body) => { val body2 = body subst(sub)
                                 binder\\body2 }
      }
      
    //}
    //  for(
    //    bibo <- self.unabs;             // TODO: use unapply pattern to
    //    val (binder, body) =  bibo; // bind (binder, body) directly
    //    body2 <- self.body subst(sub))
    //    yield (binder \\ body2)
  }    
}

}
